#!/usr/bin/python

import sys
import re

lines = sys.stdin.readlines()
lemma = sys.argv[1]

maxPriority = 101  # Maximum priority is 100

# List of ranks
rank = []
for i in range(0, maxPriority):
  rank.append([])

## EXECUTABILITY LEMMAS
if re.match('^executability', lemma):
  for line in lines:
    num = line.split(':')[0]

    if re.match('.*!S1\( .*', line): rank[100].append(num)
    elif re.match('.*St\_.*', line): rank[95].append(num)
    elif re.match('.*RcvS.*', line): rank[90].append(num)
    elif re.match('.*!KU.*\_ID.*', line): rank[20].append(num)
    elif re.match('.*!KU.*\~cid.*', line): rank[20].append(num)
    elif re.match('.*!KU.*', line): rank[85].append(num)
    else: rank[20].append(num)

## AGREEMENT LEMMAS
elif re.match('^injectiveagreement\_', lemma):

  # Injective agreement of K_gNB* (UE -> gNB)
  if (lemma == 'injectiveagreement_ue_gnb_k_gnb'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Commit\( .*', line): rank[100].append(num)
      elif re.match('.*St\_1\_UE.*', line): rank[95].append(num)
      elif re.match('.*RcvS\( .*, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*!KU\( \~K\_ASME .*', line): rank[90].append(num)
      elif re.match('.*!KU\( KDF\(\~K\_ASME,.*', line): rank[90].append(num)
      elif re.match('.*!KU\( KDF\(KDF\(\~K\_ASME,.*', line): rank[90].append(num)
      elif re.match('.*RcvS.*', line): rank[80].append(num)
      elif re.match('.*!KU\( senc.*\~K\_ASME.*', line): rank[75].append(num)
      elif re.match('.*!Handover.*', line): rank[70].append(num)
      else: rank[20].append(num)

  # Injective agreement of K_gNB* (gNB -> UE)
  elif (lemma == 'injectiveagreement_gnb_ue_k_gnb'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Commit\( .*', line): rank[100].append(num)
      elif re.match('.*St\_1\_gNB.*', line): rank[95].append(num)
      elif re.match('.*!Handover.*', line): rank[95].append(num)
      elif re.match('.*!KU\( KDF\(NH,.*', line): rank[90].append(num)
      elif re.match('.*!KU\( senc.*', line): rank[95].append(num)
      elif re.match('.*!KU\( \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*!KU\( KDF\(\~K\_ASME,.*', line): rank[95].append(num)
      elif re.match('.*!KU\( KDF\(KDF\(\~K\_ASME,.*', line): rank[95].append(num)
      elif re.match('.*RcvS.*', line): rank[80].append(num)
      elif re.match('.*St\_1\_UE.*', line): rank[75].append(num)
      else: rank[20].append(num)

## SECRECY LEMMAS
elif re.match('^secret\_', lemma):

  # Secrecy of K_ASME
  if (lemma == 'secret_k_asme'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Secret\( .*', line): rank[100].append(num)
      elif re.match('.*St\_3\_.*\( .*', line): rank[95].append(num)
      elif re.match('.*St\_2\_.*\( .*', line): rank[90].append(num)
      elif re.match('.*RcvS.*\~K\_ASME\>.*', line): rank[85].append(num)
      elif re.match('.*!KU\( \~K\_ASME \)', line): rank[80].append(num)
      elif re.match('.*RcvS.*', line): rank[75].append(num)
      else: rank[20].append(num)

  # Secrecy of K_AMF
  elif (lemma == 'secret_k_amf'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Secret\( .*', line): rank[100].append(num)
      elif re.match('.*KeyDerived\( .*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*\~K\_ASME.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*', line): rank[75].append(num)
      elif re.match('.*RcvS.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*St\_3\_.*\( .*', line): rank[95].append(num)
      elif re.match('.*St\_2\_.*\( .*', line): rank[90].append(num)
      elif re.match('.*!KU\( KDF\(\~K\_ASME.*', line): rank[80].append(num)
      elif re.match('.*!KU\( ~K\_ASME.*', line): rank[80].append(num)
      else: rank[20].append(num)

  # Secrecy of K_gNB
  elif (lemma == 'secret_k_enb'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Secret\( .*', line): rank[100].append(num)
      elif re.match('.*KeyDerived\( .*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*\~K\_ASME.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*', line): rank[75].append(num)
      elif re.match('.*RcvS.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*St\_3\_.*\( .*', line): rank[95].append(num)
      elif re.match('.*St\_2\_.*\( .*', line): rank[90].append(num)
      elif re.match('.*!KU\( KDF\(\~K\_ASME.*', line): rank[80].append(num)
      elif re.match('.*!KU\( ~K\_ASME.*', line): rank[80].append(num)
      else: rank[20].append(num)

  # Secrecy of K_eNB*
  elif (lemma == 'secret_k_gnb_star'):
    for line in lines:
      num = line.split(':')[0]

      if re.match('.*Secret\( .*', line): rank[100].append(num)
      elif re.match('.*KeyDerived\( .*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*\~K\_ASME.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*RcvS.*\'fr\_req.*', line): rank[75].append(num)
      elif re.match('.*RcvS.*\, \~K\_ASME.*', line): rank[95].append(num)
      elif re.match('.*St\_3\_.*\( .*', line): rank[95].append(num)
      elif re.match('.*St\_2\_.*\( .*', line): rank[90].append(num)
      elif re.match('.*St\_1\_.*\( .*', line): rank[85].append(num)
      elif re.match('.*!KU\( senc\(\<\'ho\_cmd.*\, KDF\(\~K\_ASME\,.*', line): rank[85].append(num)
      elif re.match('.*!KU\( senc\(\<\'ho\_cmd.*\, KDF\(\~K\_gNB\,.*', line): rank[85].append(num)
      elif re.match('.*!KU\( ~K\_ASME.*', line): rank[80].append(num)
      elif re.match('.*!KU\( KDF\(\~K\_ASME.*', line): rank[80].append(num)
      elif re.match('.*!KU\( .*KDF\(\~K\_ASME\,.*', line): rank[75].append(num)
      else: rank[20].append(num)

## UNEXPECTED LEMMAS
else:
  print "Unexpected lemma: {}".format(lemma)
  exit(0)

for goalList in reversed(rank):
  for goal in goalList:
    sys.stderr.write(goal)
    print goal
